perf: better cache sharing in `isDefEq` #8294

JovanGerb · 2025-05-12T10:52:43Z

This PR has moved to #8883

However, the effect of this change is better seen in mathlib, which has many complicated definitions, where the exponent in the exponential slowness can often get too big.

The mathlib benchmark shows

| build | -6365⬝10⁹  | -4,036 % |
| lint  | -592.7⬝10⁹ | -8,05 %  |

Zulip #lean4 > Exponential blowup in unification with metavariables @ 💬

leanprover-community-bot · 2025-05-12T12:08:41Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-05-12 12:08:40) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-05-12 14:57:36) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-05-12 23:24:36) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-05-14 20:08:19) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-05-14 22:29:55) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-05-15 02:13:08) View Log
💥 Mathlib branch lean-pr-testing-8294 build failed against this PR. (2025-06-02 17:01:36) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-02 18:28:20) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-03 11:42:15) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-03 17:34:42) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-03 21:20:18) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-04 11:20:00) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-04 18:36:06) View Log
✅ Mathlib branch lean-pr-testing-8294 has successfully built against this PR. (2025-06-07 19:16:32) View Log

This reverts commit 676b0fc.

…ntDefEq`

mattrobball · 2025-05-14T14:49:18Z

src/Lean/Meta/ExprDefEq.lean

    if (← read).inTypeClassResolution then
      -- See comment at `inTypeClassResolution`
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+      pure (i == j && m == n) <&&> checkpointDefEq (Meta.isExprDefEqAux t s)


Curious about the effect of just these changes in isDefEqProj on Mathlib.

I think just doing this change may cause a slight slowdown, because checkPointDefEq resets the transitive defEq cache. So the cache will be reset more often. I think it will work better as a fix done simultaneously with this the fix from this PR.

But I might be wrong, so feel free to try it.

This reverts commit aacf58d.

…ve to do it.

…to the previous value

perf: better cache sharing in isDefEq

ef7cccb

JovanGerb marked this pull request as draft May 12, 2025 10:52

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 12, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 12, 2025

Update lean-toolchain for testing leanprover/lean4#8294

5767dac

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025

Update lean-toolchain for testing leanprover/lean4#8294

ecfe28f

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 12, 2025

use (shareCache := true) everywhere in ExprDefEq.lean

f6881cf

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 12, 2025

Trigger CI for leanprover/lean4#8294

6f419c9

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025

Trigger CI for leanprover/lean4#8294

eb46512

leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels May 12, 2025

JovanGerb added 5 commits May 12, 2025 19:48

better management of Lean.Meta.Cache.defEqTrans

f43191b

retry CI

19c4a79

retry CI again

9964565

avoid @[extern] to resolve segfault

676b0fc

Revert "avoid @[extern] to resolve segfault"

0422dcb

This reverts commit 676b0fc.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 12, 2025

Trigger CI for leanprover/lean4#8294

6ac5d0b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025

Trigger CI for leanprover/lean4#8294

743a702

JovanGerb added 3 commits May 13, 2025 04:35

fix: bug that was already present in isDefEqProj: missing `checkPoi…

be3f48e

…ntDefEq`

retry CI

34a76d3

retry CI

2fd2cde

mattrobball reviewed May 14, 2025

View reviewed changes

JovanGerb added 2 commits May 14, 2025 19:46

move Term.addTermInfo id one line up in withRWRulesSeq

aacf58d

Revert "move Term.addTermInfo id one line up in withRWRulesSeq"

4eee7f9

This reverts commit aacf58d.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 14, 2025

Trigger CI for leanprover/lean4#8294

f227f09

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 14, 2025

Trigger CI for leanprover/lean4#8294

d396dba

fix: oh, Meta.SavedState.restore doesn't restore the cache, so I ha…

983efd6

…ve to do it.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 14, 2025

Trigger CI for leanprover/lean4#8294

b630c40

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 14, 2025

Trigger CI for leanprover/lean4#8294

d0cb3f3

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 15, 2025

Trigger CI for leanprover/lean4#8294

faa00a2

MichaelStollBayreuth mentioned this pull request May 15, 2025

Explicit ↑ can trigger slow unification #8364

Open

3 tasks

perf: instead of resetting the transient cache to be empty, reset it …

2930737

…to the previous value

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 2, 2025

Trigger CI for leanprover/lean4#8294

2211fe4

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 2, 2025

Trigger CI for leanprover/lean4#8294

72dc8c3

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jun 2, 2025

JovanGerb added 2 commits June 3, 2025 04:01

perf: don't increment numAssignments in instantiateMVars

e05d9f9

empty commit

85f2f78

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

46b2a62

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

81390cc

add a test file

244866d

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

b063966

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

7734486

JovanGerb added 2 commits June 3, 2025 20:53

set_option maxHeartbeats 1000 in test

53a4d87

slightly improve caching

cc74f96

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

4c7a43d

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 3, 2025

Trigger CI for leanprover/lean4#8294

0b3c53c

undo caching unifications that instantiate

0e96d2c

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8294

e76ab86

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8294

51dc0c9

JovanGerb added 2 commits June 4, 2025 18:03

avoid isDefEq in ExprDefEq.lean

8c514b4

empty commit

5f05587

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8294

44afc8c

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025

Trigger CI for leanprover/lean4#8294

b350f20

JovanGerb added 2 commits June 7, 2025 16:22

Merge branch 'nightly-with-mathlib' into Jovan-defEq-cache

ebb5309

empty commit

9c0429d

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 7, 2025

Trigger CI for leanprover/lean4#8294

9f00209

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 7, 2025

Trigger CI for leanprover/lean4#8294

aad4e1c

JovanGerb closed this Jun 19, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

perf: better cache sharing in `isDefEq` #8294

perf: better cache sharing in `isDefEq` #8294

Uh oh!

JovanGerb commented May 12, 2025 •

edited

Loading

Uh oh!

leanprover-community-bot commented May 12, 2025 •

edited

Loading

Uh oh!

mattrobball May 14, 2025

Uh oh!

JovanGerb May 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

perf: better cache sharing in isDefEq #8294

perf: better cache sharing in isDefEq #8294

Uh oh!

Conversation

JovanGerb commented May 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot commented May 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mattrobball May 14, 2025

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 14, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

perf: better cache sharing in `isDefEq` #8294

perf: better cache sharing in `isDefEq` #8294

JovanGerb commented May 12, 2025 •

edited

Loading

leanprover-community-bot commented May 12, 2025 •

edited

Loading